-- Modelo de memorias con cache, variante del presentado en "A Micromodularity 
-- Mechanism" (D. Jackson, I. Shlyakhter & M. Sridharan, ESEC/FSE 2001).
-- Desarrollado en clase del día 27/5/2011, Diseño de Algoritmos/Algoritmos II,
-- Dpto. de Computación, FCEFQyN, UNRC.

-- Signaturas básicas para direcciones de memorias, y datos almacenados en las 
-- mismas
sig Addr { }

sig Data { }

-- Signatura que describe una memoria, como un mapping de direcciones en datos 
-- (y su respectivo dominio)
abstract sig Memory {
    addrs: set Addr,
    map: addrs -> one Data    
}

-- Signatura que describe memorias principales, como tipos particulares de 
-- memorias.
sig MainMemory extends Memory { }

-- Signatura que describe memorias cache, en las cuales un subconjunto de las 
-- direcciones se considera "sucias", y tienen un tamaño máximo (No. de tuplas)
sig Cache extends Memory {
    dirty: set addrs,
    size: Int
}

-- Las tuplas de una cache no pueden exceder su tamaño, y el tamaño es mayor 
-- que cero
fact cacheConstraints { 
   all c: Cache | #c.addrs <= c.size &&
   c.size>0    
}

-- Un sistema consta de una memoria principal y una memoria con cache. 
-- El espacio de direcciones de la cache siempre está contenido en el de 
-- memoria principal
sig System {
    main: MainMemory,
    cache: Cache
}{
    cache.addrs in main.addrs
}

-- Invariante de sistema: si memoria principal y cache no coinciden en su 
-- contenido en una dirección, la misma está "sucia".
pred systemOK[s: System] {
    all a: s.main.addrs & s.cache.addrs |
           (s.main.map)[a] != (s.cache.map)[a] implies a in s.cache.dirty
}

run systemOK for 3 but exactly 1 System

pred show[] {
    some s: System | systemOK[s] && 
         some s.main.map && some s.cache.map
}

run show for 3 but exactly 1 System

-- Operación de flushing de memorias con cache, caracterizada como un predicado.
-- Se elige una dirección de cache, se "descarta" de la cache, y se vuelca en 
-- memoria principal si la misma es sucia.
pred flush[s, s': System] {
    some a: s.cache.addrs | 
        (a !in s.cache.dirty implies s.main.map = s'.main.map &&
                                    s'.cache.map = s.cache.map - (a -> Data) &&
                                    s'.cache.size = s.cache.size &&
                                    s'.cache.dirty = s.cache.dirty )
        &&
        (a in s.cache.dirty implies 
         s'.main.map = s.main.map ++ (a -> s.cache.map[a]) &&
         s'.cache.map = s.cache.map - (a -> Data) &&
         s'.cache.dirty = s.cache.dirty - a &&
         s'.cache.size = s.cache.size)
}

run flush for 3 but exactly 2 System 

-- Aserción: flush preserva systemOK
assert flushOK {
    all s, s': System | systemOK[s] && flush[s,s'] implies
        systemOK[s']
}

check flushOK for 30
